Generic{f:T|S(f)}
== R:((T List)Prop).
== (i:, s:T List. s':T List. s  s' & R(i,s'))
== & (f:(T). (i:. s:T List. R(i,s) & (n:||s||. s[n] = f(n)))  S(f)) 

latex

---

clarification:

generic{i:l}
generic(T; f.S(f))
== R:((T List)Prop{i}).
== (i:, s:T List. s':T List. s  s'  T List & R(i,s'))
== & (f:(T). (i:. s:T List. R(i,s) & (n:{0..||s||}. s[n] = f(n)  T))  S(f)) 

latex

Definitions	Prop, l1  l2, x:AB(x), P  Q, , x:A. B(x), type List, P & Q, x:A. B(x), {i..j}, #$n, ||as||, s = t, l[i], f(a)
FDL editor aliases	generic